Search Results

Documents authored by Manzonetto, Giulio

Document
Complete Volume
DOI: 10.4230/OASIcs.Microservices.2020-2022
OASIcs, Volume 111, Microservices 2020/2022, Complete Volume

Authors: Gokila Dorai, Maurizio Gabbrielli, Giulio Manzonetto, Aomar Osmani, Marco Prandini, Gianluigi Zavattaro, and Olaf Zimmermann

Published in: OASIcs, Volume 111, Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022)

Abstract
OASIcs, Volume 111, Microservices 2020/2022, Complete Volume
Cite as

Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022). Open Access Series in Informatics (OASIcs), Volume 111, pp. 1-156, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Proceedings{dorai_et_al:OASIcs.Microservices.2020-2022,
  title =	{{OASIcs, Volume 111, Microservices 2020/2022, Complete Volume}},
  booktitle =	{Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022)},
  pages =	{1--156},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-306-5},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{111},
  editor =	{Dorai, Gokila and Gabbrielli, Maurizio and Manzonetto, Giulio and Osmani, Aomar and Prandini, Marco and Zavattaro, Gianluigi and Zimmermann, Olaf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.Microservices.2020-2022},
  URN =		{urn:nbn:de:0030-drops-194618},
  doi =		{10.4230/OASIcs.Microservices.2020-2022},
  annote =	{Keywords: OASIcs, Volume 111, Microservices 2020/2022, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/OASIcs.Microservices.2020-2022.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Gokila Dorai, Maurizio Gabbrielli, Giulio Manzonetto, Aomar Osmani, Marco Prandini, Gianluigi Zavattaro, and Olaf Zimmermann

Published in: OASIcs, Volume 111, Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022). Open Access Series in Informatics (OASIcs), Volume 111, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{dorai_et_al:OASIcs.Microservices.2020-2022.0,
  author =	{Dorai, Gokila and Gabbrielli, Maurizio and Manzonetto, Giulio and Osmani, Aomar and Prandini, Marco and Zavattaro, Gianluigi and Zimmermann, Olaf},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022)},
  pages =	{0:i--0:xiv},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-306-5},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{111},
  editor =	{Dorai, Gokila and Gabbrielli, Maurizio and Manzonetto, Giulio and Osmani, Aomar and Prandini, Marco and Zavattaro, Gianluigi and Zimmermann, Olaf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.Microservices.2020-2022.0},
  URN =		{urn:nbn:de:0030-drops-194624},
  doi =		{10.4230/OASIcs.Microservices.2020-2022.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2023.3
A Lambda Calculus Satellite (Invited Talk)

Authors: Giulio Manzonetto

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
We shortly summarize the contents of the book "A Lambda Calculus Satellite", presented at the 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023).
Cite as

Giulio Manzonetto. A Lambda Calculus Satellite (Invited Talk). In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 3:1-3:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{manzonetto:LIPIcs.FSCD.2023.3,
  author =	{Manzonetto, Giulio},
  title =	{{A Lambda Calculus Satellite}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{3:1--3:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.3},
  URN =		{urn:nbn:de:0030-drops-179878},
  doi =		{10.4230/LIPIcs.FSCD.2023.3},
  annote =	{Keywords: \lambda-calculus, rewriting, denotational models, equational theories}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.7
Call-By-Value, Again!

Authors: Axel Kerinec, Giulio Manzonetto, and Simona Ronchi Della Rocca

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
The quest for a fully abstract model of the call-by-value λ-calculus remains crucial in programming language theory, and constitutes an ongoing line of research. While a model enjoying this property has not been found yet, this interesting problem acts as a powerful motivation for investigating classes of models, studying the associated theories and capturing operational properties semantically. We study a relational model presented as a relevant intersection type system, where intersection is in general non-idempotent, except for an idempotent element that is injected in the system. This model is adequate, equates many λ-terms that are indeed equivalent in the maximal observational theory, and satisfies an Approximation Theorem w.r.t. a system of approximants representing finite pieces of call-by-value Böhm trees. We show that these tools can be used for characterizing the most significant properties of the calculus - namely valuability, potential valuability and solvability - both semantically, through the notion of approximants, and logically, by means of the type assignment system. We mainly focus on the characterizations of solvability, as they constitute an original result. Finally, we prove the decidability of the inhabitation problem for our type system by exhibiting a non-deterministic algorithm, which is proven sound, correct and terminating.
Cite as

Axel Kerinec, Giulio Manzonetto, and Simona Ronchi Della Rocca. Call-By-Value, Again!. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kerinec_et_al:LIPIcs.FSCD.2021.7,
  author =	{Kerinec, Axel and Manzonetto, Giulio and Ronchi Della Rocca, Simona},
  title =	{{Call-By-Value, Again!}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{7:1--7:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.7},
  URN =		{urn:nbn:de:0030-drops-142458},
  doi =		{10.4230/LIPIcs.FSCD.2021.7},
  annote =	{Keywords: \lambda-calculus, call-by-value, intersection types, solvability, inhabitation}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.20
Refutation of Sallé's Longstanding Conjecture

Authors: Benedetto Intrigila, Giulio Manzonetto, and Andrew Polonsky

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract
The lambda-calculus possesses a strong notion of extensionality, called "the omega-rule", which has been the subject of many investigations. It is a longstanding open problem whether the equivalence obtained by closing the theory of Böhm trees under the omega-rule is strictly included in Morris's original observational theory, as conjectured by Sallé in the seventies. In a recent work, Breuvart et al. have shown that Morris's theory satisfies the omega-rule. In this paper we demonstrate that the two aforementioned theories actually coincide, thus disproving Sallé's conjecture.
Cite as

Benedetto Intrigila, Giulio Manzonetto, and Andrew Polonsky. Refutation of Sallé's Longstanding Conjecture. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{intrigila_et_al:LIPIcs.FSCD.2017.20,
  author =	{Intrigila, Benedetto and Manzonetto, Giulio and Polonsky, Andrew},
  title =	{{Refutation of Sall\'{e}'s Longstanding Conjecture}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.20},
  URN =		{urn:nbn:de:0030-drops-77236},
  doi =		{10.4230/LIPIcs.FSCD.2017.20},
  annote =	{Keywords: lambda calculus, observational equivalence, B\"{o}hm trees, omega-rule}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.15
New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable

Authors: Flavien Breuvart, Giulio Manzonetto, Andrew Polonsky, and Domenico Ruoppolo

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
Working in the untyped lambda calculus, we study Morris's lambda-theory H+. Introduced in 1968, this is the original extensional theory of contextual equivalence. On the syntactic side, we show that this lambda-theory validates the omega-rule, thus settling a long-standing open problem.On the semantic side, we provide sufficient and necessary conditions for relational graph models to be fully abstract for H+. We show that a relational graph model captures Morris's observational preorder exactly when it is extensional and lambda-Konig. Intuitively, a model is lambda-Konig when every lambda-definable tree has an infinite path which is witnessed by some element of the model. Both results follow from a weak separability property enjoyed by terms differing only because of some infinite eta-expansion, which is proved through a refined version of the Böhm-out technique.
Cite as

Flavien Breuvart, Giulio Manzonetto, Andrew Polonsky, and Domenico Ruoppolo. New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{breuvart_et_al:LIPIcs.FSCD.2016.15,
  author =	{Breuvart, Flavien and Manzonetto, Giulio and Polonsky, Andrew and Ruoppolo, Domenico},
  title =	{{New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{15:1--15:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.15},
  URN =		{urn:nbn:de:0030-drops-59924},
  doi =		{10.4230/LIPIcs.FSCD.2016.15},
  annote =	{Keywords: Lambda calculus, relational models, fully abstract, B\"{o}hm-out, omega-rule}
}
Document
DOI: 10.4230/LIPIcs.CSL.2011.97
Full Abstraction for Resource Calculus with Tests

Authors: Antonio Bucciarelli, Alberto Carraro, Thomas Ehrhard, and Giulio Manzonetto

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract
We study the semantics of a resource sensitive extension of the lambda-calculus in a canonical reflexive object of a category of sets and relations, a relational version of the original Scott D infinity model of the pure lambda-calculus. This calculus is related to Boudol's resource calculus and is derived from Ehrhard and Regnier's differential extension of Linear Logic and of the lambda-calculus. We extend it with new constructions, to be understood as implementing a very simple exception mechanism, and with a ``must'' parallel composition. These new operations allow to associate a context of this calculus with any point of the model and to prove full abstraction for the finite sub-calculus where ordinary lambda-calculus application is not allowed. The result is then extended to the full calculus by means of a Taylor Expansion formula.
Cite as

Antonio Bucciarelli, Alberto Carraro, Thomas Ehrhard, and Giulio Manzonetto. Full Abstraction for Resource Calculus with Tests. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 97-111, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{bucciarelli_et_al:LIPIcs.CSL.2011.97,
  author =	{Bucciarelli, Antonio and Carraro, Alberto and Ehrhard, Thomas and Manzonetto, Giulio},
  title =	{{Full Abstraction for Resource Calculus with Tests}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{97--111},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.97},
  URN =		{urn:nbn:de:0030-drops-32250},
  doi =		{10.4230/LIPIcs.CSL.2011.97},
  annote =	{Keywords: resource lambda calculus, relational semantics, full abstraction, differential linear logic}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact